(declare-fun _substvar_23_ () Bool)
(declare-fun _substvar_24_ () Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(declare-const r12 Real)
(declare-const r14 Real)
(declare-const r16 Real)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const r17 Real)
(assert (or _substvar_23_ (distinct r16 2337023.0 0.9888)))
(declare-const v5 Bool)
(assert (exists ((q7 Bool) (q8 Bool) (q9 Bool) (q10 Bool) (q11 Bool) (q12 Real) (q13 Real) (q14 Real) (q15 Bool)) (=> (=> q8 v4) (< 403160285.0 q14 q12))))
(assert (=> (distinct r16 2337023.0 0.9888) v5))
(check-sat)
